es:event_system{i:l}, e,e':es-E(es).
(loc(e) = loc(e')  Id)  (([e, e'] = []  (es-E(es) List))  es-locl(es; e'; e)) 

latex

Definitions	event_system{i:l}, t  T, x:A. B(x), es-E(es), loc(e), Id, prop{i:l}, es-locl(es; e; e'), [e, e'], P  Q, P  Q, P  Q, P  Q, ||as||, A, es-le(es; e; e'), P  Q, decidable(P), False, ge(i; j)
Lemmas	length zero, decidable int equal, non neg length, length wf1, decidable es-locl, es-le-not-locl, es-interval-non-zero, es-interval wf, es-locl wf, Id wf, es-loc wf, es-E wf, event system wf